Tofte–Talpin Type System